/*
Copyright 2008 Nicola Olivetti, Gian Luca Pozzato

    This file is part of GoalDuck.

    GoalDuck is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    GoalDuck is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with GoalDuck.  If not, see <http://www.gnu.org/licenses/>.
*/

/* Theorem prover GoalDUCK */
:- op(400,fy,neg), 
   op(500,xfy,and), 
   op(600,xfy,or),
   op(650,xfy,->), 
   op(650,yfx,=>).
:-use_module(library(lists)).


/* --------------------------------------------------------------------------------------- */

/* The following predicate implements the calculi:

   prove(G,Gamma,Labels,ProofTree) :- Gamma |- G 

   Labels is the list of labels used in that branch;
   ProofTree is the proof tree built by the system 
   and is used by the graphical interface written in Java */


/* Axioms */
prove([_,true],_,_,_,ax):-!.
prove([X,Q],Gamma,_,_,ax):-atom(Q),member([X,Q],Gamma).

/* Rules */
prove([X,G1 and G2],Gamma,Trans,Labels,tree(and,Left,Right)):-
  prove([X,G1],Gamma,Trans,Labels,Left),
  prove([X,G2],Gamma,Trans,Labels,Right).
  
prove([X,G1 or G2],Gamma,Trans,Labels,tree(or,SubTree)):-
  (prove([X,G1],Gamma,Trans,Labels,SubTree),!);prove([X,G2],Gamma,Trans,Labels,SubTree).
  
prove([X,A => G],Gamma,Trans,Labels,tree(cond,SubTree)):-  
  generaLabels(Y,Labels),
  prove([Y,G],Gamma,[[X,A,Y]|Trans],[Y|Labels],SubTree).
  
prove([X,A,Y],_,Trans,_,tree(trans,Left,Right)):-
  member([X,AP,Y],Trans),
  flat(A,DefA),
  flat(AP,DefAP),
  prove([x,A],DefAP,[],[x],Left),
  prove([x,AP],DefA,[],[x],Right).
  
prove([X,Q],Gamma,Trans,Labels,tree(propBase,SubGoal)):-
  member([X,G->Q],Gamma),
  atom(Q),
  prove([X,G],Gamma,Trans,Labels,SubGoal).

prove([X,Q],Gamma,Trans,Labels,tree(prop,SubGoal,SubTrans)):-
  member([Y,F=>(G->Q)],Gamma),
  atom(Q),
  prove([X,G],Gamma,Trans,Labels,SubGoal),
  extract(F,List),
  proveList(X,Y,List,Gamma,Trans,Labels,SubTrans).
  
/* Predicate implementing the flattening of a conjunction of formulas */
flat(P,[[x,P]]):-atom(P),!.
flat(A1 and A2,Res):-flat(A1,FlatA1),flat(A2,FlatA2),append(FlatA1,FlatA2,Res).
  
/* Auxiliary predicates to compute Uprop */
extract(Rest=>A,[A|Tail]):-!,extract(Rest,Tail).
extract(F,[F]):-!.
proveList(K,Y,[A],Gamma,Trans,Labels,SubTree):-
  prove([Y,A,K],Gamma,Trans,Labels,SubTree).
proveList(X,Y,[A|Tail],Gamma,Trans,Labels,[SubTree|SubList]):-
  prove([K,A,X],Gamma,Trans,Labels,SubTree),
  proveList(K,Y,Tail,Gamma,Trans,Labels,SubList).


/* -------------------------------------------------------------- */

/* This predicate generates a "new" label for that branch */
generaLabels(x,Labels):-true,\+member(x,Labels),!.
generaLabels(y,Labels):-true,\+member(y,Labels),!.
generaLabels(z,Labels):-true,\+member(z,Labels),!.
generaLabels(u,Labels):-true,\+member(z,Labels),!.
generaLabels(v,Labels):-true,\+member(z,Labels),!.
generaLabels(w,Labels):-true,\+member(z,Labels),!.
generaLabels(k,Labels):-true,\+member(k,Labels),!.
generaLabels(j,Labels):-true,\+member(j,Labels),!.
generaLabels(i,Labels):-true,\+member(i,Labels),!.
generaLabels(x+1,[i|_]):-!.
generaLabels(x+N1,[Last|_]):-Last=x+N,N1 is N+1,!.


/* --------------------------------------------------------------- */

/* Example: knowledge base representing a DVD recorder */

dvdrecorder(Proof):-knowledgeBase(KB),goal(Goal),
  prove(Goal,KB,[],[x],Proof).

/*  
knowledgeBase([
  [x,seton=>((setSource=>dvdIn) -> readyToRec)],
  [x,seton=>setSource=>(insertDvd->dvdIn)],
  [x,seton=>setSource=>(true->insertDvd)],
  [x,dvdIn=>(setSource -> readyToRec)]
  ]).
goal([x,(seton=>readyToRec) or (dvdIn=>readyToRec)]).

knowledgeBase([
     [x,seton=>dvdIn=>((pressRecButton=>recording)->readyToRec)],
     [x,seton=>dvdIn=>pressRecButton=>(sourceSelected->recording)],
     [x,seton=>dvdIn=>pressRecButton=>(true->sourceSelected)],
     []
  ]).
goal([x,seton=>(dvdIn=>readyToRec)]).
*/

knowledgeBase([
     [x,seton=>((pressRecButton=>recording)->readyToRec)],
     [x,seton=>pressRecButton=>(sourceSelected->recording)],
     [x,seton=>pressRecButton=>(true->sourceSelected)]
  ]).
goal([x,seton=>readyToRec]).